Left Termination of the query pattern
q(g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 198 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇔, 41 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 454 ms)
↳10 QDP
↳11 DependencyGraphProof (⇔, 0 ms)
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 QReductionProof (⇔, 0 ms)
↳16 QDP
↳17 QDPSizeChangeProof (⇔, 0 ms)
↳18 YES

(0) Obligation:

Clauses:

e(a, b).
q(X, Y) :- e(X, Y).
q(X, f(f(X))) :- ','(p(X, f(f(X))), q(X, f(X))).
q(X, f(f(Y))) :- p(X, f(Y)).
p(X, Y) :- e(X, Y).
p(X, f(Y)) :- ','(r(X, f(Y)), p(X, Y)).
r(X, Y) :- e(X, Y).
r(X, f(Y)) :- ','(q(X, Y), r(X, Y)).
r(f(X), f(X)) :- t(f(X), f(X)).
t(X, Y) :- e(X, Y).
t(f(X), f(Y)) :- ','(q(f(X), f(Y)), t(X, Y)).

Query: q(g,g)

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
q_in: (b,b)
p_in: (b,b)
r_in: (b,b)
t_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 14 less nodes.

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(7) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(P_IN_GG(x1, x2)) = x2   
POL(Q_IN_GG(x1, x2)) = x2   
POL(R_IN_GG(x1, x2)) = x2   
POL(T_IN_GG(x1, x2)) = x2   
POL(U10_gg(x1, x2, x3)) = 0   
POL(U11_gg(x1, x2)) = 0   
POL(U12_gg(x1, x2, x3)) = 0   
POL(U13_GG(x1, x2, x3)) = x2   
POL(U13_gg(x1, x2, x3)) = 0   
POL(U14_gg(x1, x2, x3)) = 0   
POL(U1_gg(x1, x2, x3)) = 0   
POL(U2_GG(x1, x2)) = 1 + x1   
POL(U2_gg(x1, x2)) = 0   
POL(U3_gg(x1, x2)) = 0   
POL(U4_gg(x1, x2, x3)) = 0   
POL(U5_gg(x1, x2, x3)) = 0   
POL(U6_GG(x1, x2, x3)) = x2   
POL(U6_gg(x1, x2, x3)) = 0   
POL(U7_gg(x1, x2, x3)) = 0   
POL(U8_gg(x1, x2, x3)) = 0   
POL(U9_GG(x1, x2, x3)) = x2   
POL(U9_gg(x1, x2, x3)) = 0   
POL(a) = 0   
POL(b) = 0   
POL(e_in_gg(x1, x2)) = 0   
POL(e_out_gg(x1, x2)) = 0   
POL(f(x1)) = 1 + x1   
POL(p_in_gg(x1, x2)) = 0   
POL(p_out_gg(x1, x2)) = 0   
POL(q_in_gg(x1, x2)) = 0   
POL(q_out_gg(x1, x2)) = 0   
POL(r_in_gg(x1, x2)) = 0   
POL(r_out_gg(x1, x2)) = 0   
POL(t_in_gg(x1, x2)) = 0   
POL(t_out_gg(x1, x2)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.

(11) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.

(13) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))

R is empty.
The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.

(15) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(17) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
    The graph contains the following edges 1 >= 1, 2 >= 1, 1 >= 2, 2 >= 2

  • Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 >= 2

  • T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
    The graph contains the following edges 1 >= 1, 2 >= 2

(18) YES